Jape is a configurable, graphical

proof assistant In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...

, originally developed by

Richard Bornat Richard Bornat (born 1944), is a British author and researcher in the field of computer science. He is also professor of Computer programming at Middlesex University. Previously he was at Queen Mary, University of London. Research Bornat's res ...

Queen Mary, University of London , mottoeng = With united powers , established = 1785 – The London Hospital Medical College1843 – St Bartholomew's Hospital Medical College1882 – Westfield College1887 – East London College/Queen Mary College , type = Public researc ...

and Bernard Sufrin the

University of Oxford , mottoeng = The Lord is my light , established = , endowment = £6.1 billion (including colleges) (2019) , budget = £2.145 billion (2019–20) , chancellor ...

. It allows user to define a

logic Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises ...

, decide how to view proofs, and much more. It works with variants of the

sequent calculus In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology i ...

and

natural deduction In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axiom ...

. It is claimedC. Kaliszyk, F. Wiedijk, M. Hendriks and F. van Raamsdonk,
Teaching logic using a state-of-the-art proof assistant
" In: H. Geuvers and P. Courtieu (eds.), ''PATE'07, International Workshop on Proof Assistants and Types in Education,'' 37–50, 2007. that Jape is the most popular program for "computer-assisted logic teaching" that involves exercises in developing proofs in

mathematical logic Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...

. The program is available for the Mac,

Unix Unix (; trademarked as UNIX) is a family of multitasking, multiuser computer operating systems that derive from the original AT&T Unix, whose development started in 1969 at the Bell Labs research center by Ken Thompson, Dennis Ritchie, and ot ...

, and

Windows Windows is a group of several proprietary graphical operating system families developed and marketed by Microsoft. Each family caters to a certain sector of the computing industry. For example, Windows NT for consumers, Windows Server for serv ...

operating systems. It is written in the

Java Java (; id, Jawa, ; jv, ꦗꦮ; su, ) is one of the Greater Sunda Islands in Indonesia. It is bordered by the Indian Ocean to the south and the Java Sea to the north. With a population of 151.6 million people, Java is the world's List ...

programming language and released under the

GNU GPL The GNU General Public License (GNU GPL or simply GPL) is a series of widely used free software licenses that guarantee end users the four freedoms to run, study, share, and modify the software. The license was the first copyleft for general us ...

References

External links

Jape Online
official distribution website
Jape

SourceForge SourceForge is a web service that offers software consumers a centralized online location to control and manage open-source software projects and research business software. It provides source code repository hosting, bug tracking, mirrorin ...

portal Proof assistants Free theorem provers {{software-stub

See also

References

External links